(*************************************************************************)
(** Simply-typed Scalina  in Coq.    Infrastructure                      *)
(** Author: Adriaan Moors, 2008                                          *)
(*************************************************************************)

(** Based on the Coq tutorial at POPL 2008, see
    "Engineering Formal Metatheory", Aydemir, Charguéraud, Pierce,
    Pollack, Weirich. POPL 2008.

    Tutorial authors: Brian Aydemir and Stephanie Weirich, with help
    from Aaron Bohannon, Nate Foster, Benjamin Pierce, Jeffrey
    Vaughan, Dimitrios Vytiniotis, and Steve Zdancewic.  Adapted from
    code by Arthur Charguéraud.
*)

Set Implicit Arguments.
Require Import Metatheory Scalina_Definitions Scalina_Induction support.
Require Import List.

(* ********************************************************************** *)
(** ** Properties of Well-formedness and Freshness *)

Hint Constructors wf_env.

Section WfEnvProperties. (* TODO *)
Implicit Types E F : env.

Lemma wf_env_implies_ok: forall E,
  wf_env E -> ok E.
Proof.
  intros. induction H. auto. auto*.
Qed.

(* used in typing_weaken *)
Lemma splice_wf_env: forall E F G x T,
   wf_env (E & F & G)
-> wf_env (E & G & x ~ T)
-> x # F
-> wf_env (E & F & G & x ~ T).
Proof.
  intros.
  inversions* H0.  
Qed.

Lemma wf_env_inv_type_dep: forall E x T z,
  wf_env E -> binds x T E -> z # E -> z \notin fv_tp T.
Proof.
  intros.
  induction H. inversions* H0.
  binds_cases H0. 
    simpl in *. env_fix. apply IHwf_env; auto*.
    subst. apply (H3 z); auto*.
Qed.

(** Inversion for wf_env on concat *)
(*
Lemma wf_env_concat_inv : forall E F,
  wf_env (E & F) -> wf_env E /\ wf_env F.
Proof. 
  induction F as [|(x,a)]; simpl; env_fix; intros Ok.
  auto*.
  inversions Ok. split. auto*. apply* wf_env_push. 
Qed.
  *)
(** Removing bindings preserves wf_env *)

Lemma wf_env_remove : forall F E G,
  (forall x, x # G -> x # F) -> wf_env (E & F & G) -> wf_env (E & G).
Proof.
  introv HFr.
  induction G as [|(y,a)]; simpl; env_fix; intros Ok.
    induction F as [|(y,a)]; simpl.
      auto. 
      simpl in IHF. apply IHF. intros. env_fix. assert (x # F & y ~ a). auto*. auto*.
      inversions* Ok. 
    inversions* Ok. 
      assert (y # E & G) by auto*.
      apply wf_env_cons. apply IHG. 
        intros. destruct (x == y). subst. auto*. auto*. auto*. auto*.
        intros. apply H4. destruct (x == y). auto*. assert (x # F). apply HFr. auto*. auto*.
Qed.

Lemma wf_env_remove2 : forall E F,
  wf_env (E & F) -> wf_env E.
Proof.
  induction F as [|(y,a)]; simpl; env_fix; intros Ok. 
    trivial. 
    apply IHF. inversions* Ok.
Qed.


(** A binding in the middle of an environment has a var fresh
  from all the bindings before it *)

Lemma fresh_mid : forall E F x a,
  wf_env (E & x ~ a & F) -> x # E.
Proof.
  induction F; simpl; introv Ok; inversions Ok; env_fix.
    auto.
    inversions H1; env_fix.
     contradiction (eq_empty_inv H0).
     simpls*.
Qed.

Lemma fresh_mid_right:
  forall E F (x : var) a,
  wf_env (E & x ~ a & F) -> x # F.
Proof.
  introv. 
  induction F.
    intros. simpl. auto.
    intros. inversion H. subst a0.
    destruct (x == x0).
      subst x. auto*. 
      simpl. 
      assert (x # F).
        apply IHF. 
          auto*. 
      auto*. 
Qed.

End WfEnvProperties.

(** Automation *)

Hint Resolve fresh_mid fresh_mid_right.

Hint Extern 1 (wf_env (?E)) =>
  match goal with H: context [E & ?F] |- _ =>
    apply (@wf_env_remove2 _ F) end.

(* end properties of wf_env (derived from Metatheory_env) *)